Section: New Results

Distributed algorithms

Formal model and proofs for Netlog protocols

Participants : Meixian Chen, Jean-François Monin.

Joint work with Yuxin Deng (Jiaotong University, Shanghai) and Stéphane Grumbach (LIAMA/Netquest).

Netlog is a language designed and implemented in the Netquest project for describing protocols. Netlog has a precise semantics, provides a high level of abstraction thanks to its Datalog flavor and benefits from an efficient implementation. This makes it a very interesting target language for proofs of protocols. Netlog comes with two possible semantics: a synchronous semantics, better suited to tightly coupled parallel systems and an asynchronous semantics, better suited to distributed systems.

We designed a formal model of Netlog in Coq, where the two possible semantics are derived from common basic blocks. In a fully certified framework, a formal proof of the Netlog engine (running on each node) would be required. We don't attack this part at the moment: we assume that the implementation respects the general properties stated in our model and focus on the issues raised by the distributed model of computation provided by Netlog.

As a proof of concept, we applied in 2010 this framework to an algorithm constructing a Breadth-First Search Spanning Tree (BFS) in a distributed system [46] . This work has been slightly improved this year and published in [19] .

Moreover, we generalized the model in order to take the removal of datalog facts into account, and started to use this feature for more complicated protocols. In main one under study is Prim's algorithm (publication under submission), and we target next GHS, which still resists to palatable proof techniques.